es:event_system{i:l}, l:IdLnk, tgs:(Id List), da:fpf(Knd; k.Type),
f1,f2:({e:es-E(es)| loc(e) = source(l)  Id} ((tg:Id
f1,f2:({e:es-E(es)| loc(e) = source(l)  Id} ( fpf-cap(da; Kind-deq; rcv(l,tg); void)) List)),
ds1,ds2:fpf(Id; x.Type).
fpf-sub(Id; x.Type; id-deq; ds2; ds1)
 (e:{e:es-E(es)| loc(e) = source(l)  Id} . f1(e) = f2(e))
 with decls ds1 dasends on l from e include f1(e) and only these for tags in tgs
 with decls ds2 dasends on l from e include f2(e) and only these for tags in tgs 

latex

Definitions

x:A. B(x), P  Q, x(s), with decls ds dasends on l from e include f(e) and only these for tags in tgs, A c B, P  Q, t  T, prop{i:l}, x. t(x), fpf-cap(f; eq; x; z), top, if b then t else f fi , tt, ff, alle-at(es; i; e.P(e)), sq_type(T), guard(T), T, True, P  Q, P  Q, decidable(P), P  Q, Id, A, , Unit, False, int_seg(i; j),

Lemmas

es-sends-iff wf, es-E wf, Id wf, es-loc wf, lsrc wf, assert wf, es-isrcv wf, IdLnk wf, es-lnk wf, l member wf, es-tag wf, es-valtype wf, fpf-cap wf, Knd wf, Kind-deq wf, es-kind wf, es-vartype wf, id-deq wf, top wf, rcv wf, fpf-sub wf, fpf wf, event system wf, subtype rel transitivity, subtype rel self, decidable assert, fpf-dom wf, fpf-trivial-subtype-top, fpf-cap functionality wrt sub, bool wf, eqtt to assert, iff transitivity, bnot wf, not wf, eqff to assert, assert of bnot, deq wf, length wf1, squash wf, true wf, es-loc-sender, ldst wf, es-index wf, int seg wf, es-Msgl wf, es-sends wf, es-sender wf, select wf, le wf, non neg length